0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 7 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
appA_in_aag([], T5, T5) → appA_out_aag([], T5, T5)
appA_in_aag(.(T10, []), T20, .(T10, T20)) → appA_out_aag(.(T10, []), T20, .(T10, T20))
appA_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
appA_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, appA_out_aag(T64, T65, T63)) → appA_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, appA_out_aag(T33, T34, T32)) → appA_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
appA_in_aag([], T5, T5) → appA_out_aag([], T5, T5)
appA_in_aag(.(T10, []), T20, .(T10, T20)) → appA_out_aag(.(T10, []), T20, .(T10, T20))
appA_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
appA_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, appA_out_aag(T64, T65, T63)) → appA_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, appA_out_aag(T33, T34, T32)) → appA_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPA_IN_AAG(T33, T34, T32)
APPA_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
appA_in_aag([], T5, T5) → appA_out_aag([], T5, T5)
appA_in_aag(.(T10, []), T20, .(T10, T20)) → appA_out_aag(.(T10, []), T20, .(T10, T20))
appA_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
appA_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, appA_out_aag(T64, T65, T63)) → appA_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, appA_out_aag(T33, T34, T32)) → appA_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPA_IN_AAG(T33, T34, T32)
APPA_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
appA_in_aag([], T5, T5) → appA_out_aag([], T5, T5)
appA_in_aag(.(T10, []), T20, .(T10, T20)) → appA_out_aag(.(T10, []), T20, .(T10, T20))
appA_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
appA_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, appA_out_aag(T64, T65, T63)) → appA_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, appA_out_aag(T33, T34, T32)) → appA_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPA_IN_AAG(T33, T34, T32)
appA_in_aag([], T5, T5) → appA_out_aag([], T5, T5)
appA_in_aag(.(T10, []), T20, .(T10, T20)) → appA_out_aag(.(T10, []), T20, .(T10, T20))
appA_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, appA_in_aag(T33, T34, T32))
appA_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, appA_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, appA_out_aag(T64, T65, T63)) → appA_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, appA_out_aag(T33, T34, T32)) → appA_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPA_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPA_IN_AAG(T33, T34, T32)
APPA_IN_AAG(.(T10, .(T29, T32))) → APPA_IN_AAG(T32)
From the DPs we obtained the following set of size-change graphs: